package ch.epfl.lara.pm.analyze;


import ch.epfl.lara.pm.ast.{Formula,And,Or,Neg,BFalse,BTrue,In,Set,Intersection,Term}
import ch.epfl.lara.pm.ast.{True,Expr,Not,EAnd,EOr,False}

trait FormulaBuilder extends Proposition {

  def cnfFormulae(atoms: List[List[Formula]]): Formula =
    cnf[Formula](BTrue,And _, Or _)(atoms)
   
    
  def dnfFormulae(atoms: List[List[Formula]]): Formula =
    dnf[Formula](BFalse,Or _, And _)(atoms)
  
  def dnfSets(atoms: List[List[String]]): Formula = 
    dnf[Formula](BFalse,Or _, And _)(atoms.map(cartesianSet(_)))
  
  def dnfExprs(atoms: List[Expr]): Expr = 
    atoms.foldRight[Expr](False)((a,acc) => EOr(a,acc)) 
  
  
  def conjunctionSet(set: List[String]): Formula = conjunctionFormulae(cartesianSet(set))
  
  def conjunctionMultiSet(set: List[List[String]]): Formula = conjunctionFormulae(cartesianMultiSet(set))
  
  def conjunctionFormulae(forms: List[Formula]): Formula = conjunction[Formula](And _)(forms)
  
  def conjunctionExprs(atoms: List[Expr]): Expr =
    conjunction[Expr](EAnd _)(atoms)
 
    
  def disjointUnionExpr(formulaA: Expr, formulaB: Expr): Expr = 
    disjointUnion[Expr](Not _, EAnd _)(formulaA,formulaB)
  
  def disjointUnionFormula(setA: Formula, setB: Formula): Formula = 
    disjointUnion[Formula](Neg _, And _)(setA,setB)
    
  def disjointUnionSet(setA: List[String], setB: List[String]): Formula = 
    disjointUnionFormula(conjunctionSet(setA),conjunctionSet(setB))

  
  
    
  def disjointSets(sets: List[List[String]]): List[Formula] = 
    disjointFormulae(cartesianSets(sets))
  
  
  def disjointFormulae(sets: List[Formula]): List[Formula] = 
    disjoint(disjointUnionFormula)(sets)
  
    
  def disjointExprs(sets: List[Expr]): List[Expr] = 
    disjoint(disjointUnionExpr)(sets)
  
    
    
  
  def cartesianSet(set: List[String]): List[Formula] = {
    val elements = Util.letters.take(set.length).force
    assert(set.length == elements.length)
    elements.zip(set).map(makeSetProposition(_))
  }
 
  def cartesianMultiSet(mset: List[List[String]]): List[Formula] = {
    val elements = Util.letters.take(mset.length).force
    assert(mset.length == elements.length)
    val fsets = for(set<-mset) yield {
      val nset = set.removeDuplicates
      if(nset.size > 1) nset.map(Set(_)).reduceRight[Term]((a,b)=>Intersection(a,b))
      else Set(nset.head)
    }
    elements.zip(fsets).map(pair => In(pair._1,pair._2))
  }
  

  def cartesianSets(sets: List[List[String]]): List[Formula] = 
    sets.map(set => conjunctionFormulae(cartesianSet(set)))
  
  
  def makeSetProposition(pair: (String,String)): In = makeSetProposition(pair._1, pair._2)
  
  def makeSetProposition(varname: String, setname: String): In = In(varname,Set(setname))
  
  
  
  
}
